Actario: A Framework for Reasoning About Actor Systems

Shohei Yasutake, Takuo Watanabe

Coq:
CoFixpoint behvA := receive (fun msg ⇒
match msg with
| name_msg sender ⇒ me ← self; sender ! name_msg me; become behvA
|_⇒ child ← new behvB; child ! msg; become behvA
end)

Erlang:
behvA() → receive Msg → case Msg of
{name_msg, Sender} → Me = self(), Sender ! {name_msg, Me}, behvA()
     _ → Child = spawn(fun() → behvB() end), Child ! Msg behvA()
end.

_______________
[1] http://amutake.github.io/actario/AGERE2015.pdf